the_es:event_system{i:l}, e:es-E(the_es).
((es-first(the_es; e)))  (es-pred(the_es; e)  es-E(the_es)) 

latex

Definitions	t  T, x:A. B(x), first(e), b, A, P  Q, pred(e), P  Q, es-pred?(es), es-pred(es; e), es-E(es), es-first(es; e), x:A  B(x), event_system{i:l}, x:AB(x)
Lemmas	event system wf, pred wf, not wf, assert wf, first wf